\begin{tabbing}
$\forall$${\it es}$:ES, $T$:Type, $i$:Id, $P$:($T$$\rightarrow\mathbb{P}$), $Q$:(E$\rightarrow$$T$$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$x$:$T$. Dec($P$($x$)))
\\[0ex]$\Rightarrow$ \=($\forall$$L$:($T$ List).\+
\\[0ex]($\forall$$x$$\in$$L$. $\forall$$e$:E. $Q$($e$,$x$) $\Rightarrow$ (loc($e$) = $i$ $\in$ Id))
\\[0ex]$\Rightarrow$ ($\forall$$x$$\in$$L$. $P$($x$) $\Rightarrow$ ($\exists$$e$:E. $Q$($e$,$x$)))
\\[0ex]$\Rightarrow$ (($\neg$($\exists$$x$$\in$$L$.$P$($x$))) $\Rightarrow$ $\exists$${\it e'}$@$i$.True)
\\[0ex]$\Rightarrow$ $\exists$${\it e'}$@$i$.$\forall$$x$$\in$$L$. $P$($x$) $\Rightarrow$ ($\exists$$e$:E. ($e$ $\leq$loc ${\it e'}$  \& $Q$($e$,$x$))))
\-
\end{tabbing}